|
In constructive mathematics, Church's thesis (CT) is an axiom which states that all total functions are computable. The axiom takes its name from the Church–Turing thesis, which states that every effectively calculable function is a computable function, but the constructivist version is much stronger, claiming that every function is computable. The axiom CT is incompatible with classical logic in sufficiently strong systems. For example, Heyting arithmetic (HA) with CT as an addition axiom is able to disprove some instances of the law of the excluded middle. However, Heyting arithmetic is equiconsistent with Peano arithmetic (PA) as well as with Heyting arithmetic plus Church's thesis. That is, adding either the law of the excluded middle or Church's thesis does not make Heyting arithmetic inconsistent, but adding both does. ==Formal statement== In first-order theories such as HA, which cannot quantify over functions directly, CT is stated as an axiom schema which says that any definable function is computable, using Kleene's T predicate to define computability. For each formula φ(''x'',''y'') of two variables, the schema includes the axiom : This axiom asserts that, if for every ''x'' there is a ''y'' satisfying φ then there is in fact an ''e'' which is the Gödel number of a general recursive function that will, for every ''x'', produce such a ''y'' satisfying the formula, with some ''u'' being a Gödel number encoding a verifiable computation bearing witness to the fact that ''y'' is in fact the value of that function at ''x''. In higher-order systems that can quantify over functions directly, CT can be stated as a single axiom which says that every function from the natural numbers to the natural numbers is computable. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Church's thesis (constructive mathematics)」の詳細全文を読む スポンサード リンク
|